es:ES, i:Id, R:({e:E| loc(e) = i }Prop), e:E.
(e:E. loc(e) = i  Dec(R(e)))
 loc(e) = i
 (e':E. e'  e  & R(e'))
 (e':E. e'  e  & R(e') & (e'':E. (e' <loc e'')  e''  e   R(e''))) 

latex

Definitions	t  T, x:A. B(x), E, b, P  Q, False, A, x:A. B(x), P & Q, (e <loc e'), loc(e), Id, x(s), e  e' , Prop, A & B, Dec(P), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, P  Q, P  Q, first(e), True, T, 1of(t), pred(e), P  Q
Lemmas	member wf, es-pred wf, es-pred-locl, es-le-iff, squash wf, true wf, decidable assert, es-first wf, es-le-not-locl, es-le-self, event system wf, es-locl-wellfnd, decidable wf, es-locl wf, es-le wf, not wf, Id wf, es-loc wf, es-le-loc, es-loc-pred, es-E wf